Left Termination of the query pattern log2_in_2(a, g) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

log2(X, Y) :- log2(X, 0, s(0), Y).
log2(s(s(X)), Half, Acc, Y) :- log2(X, s(Half), Acc, Y).
log2(X, s(s(Half)), Acc, Y) :- ','(small(X), log2(Half, s(0), s(Acc), Y)).
log2(X, Half, Y, Y) :- ','(small(X), small(Half)).
small(0).
small(s(0)).

Queries:

log2(a,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
log2_in: (f,b)
log2_in: (f,b,b,b) (b,b,b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x5)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x4)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x2, x4)
SMALL_IN_A(x1)  =  SMALL_IN_A
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x5)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x5)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x5)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x4)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U1_AG(x1, x2, x3)  =  U1_AG(x3)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x5)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x4)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x2, x4)
SMALL_IN_A(x1)  =  SMALL_IN_A
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x5)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x5)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x5)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x4)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U1_AG(x1, x2, x3)  =  U1_AG(x3)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 18 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_GGGG(Half, Acc, Y, small_out_g) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(Half, Acc, Y, small_in_g(X))

The TRS R consists of the following rules:

small_in_g(0) → small_out_g
small_in_g(s(0)) → small_out_g

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

Strictly oriented rules of the TRS R:

small_in_g(s(0)) → small_out_g

Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0   
POL(LOG2_IN_GGGG(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(U3_GGGG(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(s(x1)) = 1 + x1   
POL(small_in_g(x1)) = 2 + x1   
POL(small_out_g) = 2   



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                          ↳ QDP
                            ↳ DependencyGraphProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_GGGG(Half, Acc, Y, small_out_g) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(Half, Acc, Y, small_in_g(X))

The TRS R consists of the following rules:

small_in_g(0) → small_out_g

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x2, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y) we obtained the following new rules:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2) we obtained the following new rules:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
                              ↳ QDP
                                ↳ NonTerminationProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

The TRS R consists of the following rules:none


s = LOG2_IN_AGGG(s(s(z0)), z1, z2) evaluates to t =LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG2_IN_AGGG(s(s(z0)), z1, z2) to LOG2_IN_AGGG(s(s(s(z0))), z1, z2).




We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
log2_in: (f,b)
log2_in: (f,b,b,b) (b,b,b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x1, x2, x3, x4, x5)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x1, x2, x3, x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x3, x4)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x1, x2, x3, x4)
SMALL_IN_A(x1)  =  SMALL_IN_A
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x1, x2, x3, x4, x5)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x2, x3, x4, x5)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x2, x3, x4)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AG(X, Y) → U1_AG(X, Y, log2_in_aggg(X, 0, s(0), Y))
LOG2_IN_AG(X, Y) → LOG2_IN_AGGG(X, 0, s(0), Y)
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → U2_AGGG(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → U3_AGGG(X, Half, Acc, Y, small_in_a(X))
LOG2_IN_AGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_A(X)
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → U4_AGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_AGGG(X, Half, Acc, Y, small_out_a(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → U2_GGGG(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → SMALL_IN_G(X)
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → U4_GGGG(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(X, Half, Y, Y) → U5_GGGG(X, Half, Y, small_in_g(X))
LOG2_IN_GGGG(X, Half, Y, Y) → SMALL_IN_G(X)
U5_GGGG(X, Half, Y, small_out_g(X)) → U6_GGGG(X, Half, Y, small_in_g(Half))
U5_GGGG(X, Half, Y, small_out_g(X)) → SMALL_IN_G(Half)
LOG2_IN_AGGG(X, Half, Y, Y) → U5_AGGG(X, Half, Y, small_in_a(X))
LOG2_IN_AGGG(X, Half, Y, Y) → SMALL_IN_A(X)
U5_AGGG(X, Half, Y, small_out_a(X)) → U6_AGGG(X, Half, Y, small_in_g(Half))
U5_AGGG(X, Half, Y, small_out_a(X)) → SMALL_IN_G(Half)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x1, x2, x3, x4, x5)
U6_GGGG(x1, x2, x3, x4)  =  U6_GGGG(x1, x2, x3, x4)
U5_AGGG(x1, x2, x3, x4)  =  U5_AGGG(x2, x3, x4)
U5_GGGG(x1, x2, x3, x4)  =  U5_GGGG(x1, x2, x3, x4)
SMALL_IN_A(x1)  =  SMALL_IN_A
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x1, x2, x3, x4, x5)
LOG2_IN_AG(x1, x2)  =  LOG2_IN_AG(x2)
SMALL_IN_G(x1)  =  SMALL_IN_G(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x1, x2, x3, x4, x5)
U6_AGGG(x1, x2, x3, x4)  =  U6_AGGG(x1, x2, x3, x4)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U3_AGGG(x1, x2, x3, x4, x5)  =  U3_AGGG(x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 18 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
LOG2_IN_GGGG(x1, x2, x3, x4)  =  LOG2_IN_GGGG(x1, x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5)  =  U3_GGGG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

LOG2_IN_GGGG(X, s(s(Half)), Acc, Y) → U3_GGGG(X, Half, Acc, Y, small_in_g(X))
LOG2_IN_GGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_GGGG(X, s(Half), Acc, Y)


Used ordering: POLO with Polynomial interpretation [25]:

POL(0) = 0   
POL(LOG2_IN_GGGG(x1, x2, x3, x4)) = 2·x1 + 2·x2 + x3 + x4   
POL(U3_GGGG(x1, x2, x3, x4, x5)) = 1 + x1 + 2·x2 + x3 + x4 + x5   
POL(s(x1)) = 1 + x1   
POL(small_in_g(x1)) = 2 + x1   
POL(small_out_g(x1)) = 2 + x1   



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
                          ↳ QDP
                            ↳ DependencyGraphProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U3_GGGG(X, Half, Acc, Y, small_out_g(X)) → LOG2_IN_GGGG(Half, s(0), s(Acc), Y)

The TRS R consists of the following rules:

small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))

The set Q consists of the following terms:

small_in_g(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

The TRS R consists of the following rules:

log2_in_ag(X, Y) → U1_ag(X, Y, log2_in_aggg(X, 0, s(0), Y))
log2_in_aggg(s(s(X)), Half, Acc, Y) → U2_aggg(X, Half, Acc, Y, log2_in_aggg(X, s(Half), Acc, Y))
log2_in_aggg(X, s(s(Half)), Acc, Y) → U3_aggg(X, Half, Acc, Y, small_in_a(X))
small_in_a(0) → small_out_a(0)
small_in_a(s(0)) → small_out_a(s(0))
U3_aggg(X, Half, Acc, Y, small_out_a(X)) → U4_aggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(s(s(X)), Half, Acc, Y) → U2_gggg(X, Half, Acc, Y, log2_in_gggg(X, s(Half), Acc, Y))
log2_in_gggg(X, s(s(Half)), Acc, Y) → U3_gggg(X, Half, Acc, Y, small_in_g(X))
small_in_g(0) → small_out_g(0)
small_in_g(s(0)) → small_out_g(s(0))
U3_gggg(X, Half, Acc, Y, small_out_g(X)) → U4_gggg(X, Half, Acc, Y, log2_in_gggg(Half, s(0), s(Acc), Y))
log2_in_gggg(X, Half, Y, Y) → U5_gggg(X, Half, Y, small_in_g(X))
U5_gggg(X, Half, Y, small_out_g(X)) → U6_gggg(X, Half, Y, small_in_g(Half))
U6_gggg(X, Half, Y, small_out_g(Half)) → log2_out_gggg(X, Half, Y, Y)
U4_gggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_gggg(X, s(s(Half)), Acc, Y)
U2_gggg(X, Half, Acc, Y, log2_out_gggg(X, s(Half), Acc, Y)) → log2_out_gggg(s(s(X)), Half, Acc, Y)
U4_aggg(X, Half, Acc, Y, log2_out_gggg(Half, s(0), s(Acc), Y)) → log2_out_aggg(X, s(s(Half)), Acc, Y)
log2_in_aggg(X, Half, Y, Y) → U5_aggg(X, Half, Y, small_in_a(X))
U5_aggg(X, Half, Y, small_out_a(X)) → U6_aggg(X, Half, Y, small_in_g(Half))
U6_aggg(X, Half, Y, small_out_g(Half)) → log2_out_aggg(X, Half, Y, Y)
U2_aggg(X, Half, Acc, Y, log2_out_aggg(X, s(Half), Acc, Y)) → log2_out_aggg(s(s(X)), Half, Acc, Y)
U1_ag(X, Y, log2_out_aggg(X, 0, s(0), Y)) → log2_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
log2_in_ag(x1, x2)  =  log2_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
log2_in_aggg(x1, x2, x3, x4)  =  log2_in_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
s(x1)  =  s(x1)
U3_aggg(x1, x2, x3, x4, x5)  =  U3_aggg(x2, x3, x4, x5)
small_in_a(x1)  =  small_in_a
small_out_a(x1)  =  small_out_a(x1)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x1, x2, x3, x4, x5)
log2_in_gggg(x1, x2, x3, x4)  =  log2_in_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
U3_gggg(x1, x2, x3, x4, x5)  =  U3_gggg(x1, x2, x3, x4, x5)
small_in_g(x1)  =  small_in_g(x1)
0  =  0
small_out_g(x1)  =  small_out_g(x1)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
U5_gggg(x1, x2, x3, x4)  =  U5_gggg(x1, x2, x3, x4)
U6_gggg(x1, x2, x3, x4)  =  U6_gggg(x1, x2, x3, x4)
log2_out_gggg(x1, x2, x3, x4)  =  log2_out_gggg(x1, x2, x3, x4)
log2_out_aggg(x1, x2, x3, x4)  =  log2_out_aggg(x1, x2, x3, x4)
U5_aggg(x1, x2, x3, x4)  =  U5_aggg(x2, x3, x4)
U6_aggg(x1, x2, x3, x4)  =  U6_aggg(x1, x2, x3, x4)
log2_out_ag(x1, x2)  =  log2_out_ag(x1, x2)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(X)), Half, Acc, Y) → LOG2_IN_AGGG(X, s(Half), Acc, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2_IN_AGGG(x1, x2, x3, x4)  =  LOG2_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN_AGGG(Half, Acc, Y) → LOG2_IN_AGGG(s(Half), Acc, Y) we obtained the following new rules:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule LOG2_IN_AGGG(s(z0), z1, z2) → LOG2_IN_AGGG(s(s(z0)), z1, z2) we obtained the following new rules:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
                              ↳ QDP
                                ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

LOG2_IN_AGGG(s(s(z0)), z1, z2) → LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

The TRS R consists of the following rules:none


s = LOG2_IN_AGGG(s(s(z0)), z1, z2) evaluates to t =LOG2_IN_AGGG(s(s(s(z0))), z1, z2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LOG2_IN_AGGG(s(s(z0)), z1, z2) to LOG2_IN_AGGG(s(s(s(z0))), z1, z2).